\begin{tabbing}
fair{-}fifo\=\{i:l\}\+
\\[0ex]($w$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(\=$\forall$$i$:Id, $t$:$\mathbb{N}$, $l$:IdLnk.\+\+
\\[0ex]$\neg$source($l$) $=$ $i$ $\in$ Id $\Rightarrow$ onlnk($l$;w{-}m($w$; $i$; $t$)) $=$ nil $\in$ w{-}Msg($w$) List)
\-\\[0ex]\& (\=$\forall$$i$:Id, $t$:$\mathbb{N}$.\+
\\[0ex]w{-}isnull($w$; w{-}a($w$; $i$; $t$))
\\[0ex]$\Rightarrow$ \=($\forall$$x$:Id. w{-}s($w$; $i$; ($t$+1); $x$) $=$ w{-}s($w$; $i$; $t$; $x$) $\in$ w{-}vartype($w$; $i$; $x$))\+
\\[0ex]\& w{-}m($w$; $i$; $t$) $=$ nil $\in$ w{-}Msg($w$) List)
\-\-\\[0ex]\& \=(\=$\forall$$i$:Id, $t$:$\mathbb{N}$, $l$:IdLnk.\+\+
\\[0ex]w{-}isrcvl($w$; $l$; w{-}a($w$; $i$; $t$))
\\[0ex]$\Rightarrow$ \=destination($l$) $=$ $i$ $\in$ Id\+
\\[0ex]\& \=$\parallel$w{-}queue($w$; $l$; $t$)$\parallel\geq$1\+
\\[0ex]\& hd(w{-}queue($w$; $l$; $t$)) $=$ w{-}msg($w$; w{-}a($w$; $i$; $t$)) $\in$ w{-}Msg($w$))
\-\-\-\\[0ex]\& \=(\=$\forall$$l$:IdLnk, $t$:$\mathbb{N}$.\+\+
\\[0ex]$\exists$${\it t'}$:$\mathbb{N}$.
\\[0ex]$t$$\leq$${\it t'}$
\\[0ex]\& \=w{-}isrcvl($w$; $l$; w{-}a($w$; destination($l$); ${\it t'}$))\+
\\[0ex]$\vee$ w{-}queue($w$; $l$; ${\it t'}$) $=$ nil $\in$ w{-}Msg($w$) List)
\-\-\\[0ex]\& w{-}machine{-}constraint($w$)
\\[0ex]\& w{-}atom{-}constraint\=\{i:l\}\+
\\[0ex]($w$)
\-\-\-\-
\end{tabbing}